$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:fpf($A$; $x$.$B$($x$)), $C$:Type, $a$:($A$$\rightarrow$(?$C$)), $b$:($C$$\rightarrow$$A$), $y$:$C$.
\\[0ex]($y$ $\in$ fpf{-}domain(compose{-}fpf($a$; $b$; $f$)))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$$x$:$A$. (($x$ $\in$ fpf{-}domain($f$)) $\wedge$ (($\uparrow$isl($a$($x$))) c$\wedge$ ($y$ = outl($a$($x$))))))